i:Id, L:Id List, k:Knd.
@i: k affects only members of L 
realizes es.
e@i.
kind(e) = k
 (x:Id.
 (((x after e) = (x when e)  vartype(i;x)  (x  L))
 (& ((x  L)  (x after e) = (x when e)  vartype(i;x))) 

latex

Definitions	x:A. B(x), t  T, x. t(x), Prop, P  Q, P & Q, T, True, x(s), es is an event system of D, x:A. B(x)
Lemmas	d-realizes2-implies-realizes, d-single-aframe wf, Knd wf, Id wf, alle-at wf, es-kind wf, not wf, es-vartype wf, es-after wf, squash wf, true wf, event system wf, es-when wf, l member wf, es-E wf, es-loc wf